1. Field of the Invention
The present invention relates to an information processing apparatus as a computer system composed of a computer, in particular, to a program verifying system for verifying a program code of a primitive machine instruction set of computer software, a method thereof, and a storage medium from which a computer can read a program that causes the computer to perform the program verifying method.
2. Description of the Related Art
A program verifying method for verifying a program code during or before the execution of the program is disclosed in Japanese Patent Laid-Open Publication No.Hei-8-234994. Hereinafter, this related art reference is referred to as first conventional method. In the first conventional method, the verifying method for a program code of an interpreter type program is described.
In the first conventional method, a computer program of a server computer A that operates on an operating system A is downloaded to a user computer B that operates on an operating system B. When the user computer B checks the program code as a pre-process, if the computer B finds an instruction with a type other than restricted types from the program code of the server computer A, the instruction is prohibited from being really executed by the user computer B.
In the first conventional method, all branch instructions are checked from the program code. Stack snapshots of all branch instructions are stored in a storing portion. In the first conventional method, a pre-executing process is performed with the same data type as the main executing process for the program code. The executed state is reflected to a virtual stack of which only the data type of the program code has been simulated. The pre-executing process is successively performed from the beginning of the program. At a program position having the snapshot storing portion, data in the virtual stack is stored thereto.
In the case of a branch instruction, data in the virtual stack is stored to a snapshot storing portion of a branch destination instruction. When another instruction is executed, if data of the virtual stack is stored to the same snapshot storing portion, data of the virtual stack is compared with the stored data. When there is a difference between the snapshot and the virtual stack, the execution is prohibited. Thus, the data type of each instruction of a program code including a froward branch instruction and a backward branch instruction can be checked.
However, in the first conventional method, it is presumed that each instruction of a program code has one restriction against the type of a data stack. When there is a restriction of which only data of A type or data of B type can be dealt for an instruction X, data of A type is stored as a particular snapshot. Thereafter, when data of B type is stored as the snapshot, the program code that is not harmful is prohibited from being executed.
For a problem of which a restriction range is not uniquely settled, another related art reference has proposed one solution (refer to xe2x80x9cThe Java Virtual Machine Specification,xe2x80x9d Sun Microsystems Inc, pp. 125-137). Hereinafter, this related art reference is referred to as second conventional method.
In the second conventional method, when a plurality of different data types should exist in the same snapshot, a data type that contains all the data types is decided. The new data type is stored as a new snapshot. With the decided data type, the program code is re-executed from the new snapshot position. Thus, the data type is re-checked.
However, the program code type verifying methods in the first conventional method and the second conventional method have the following problems. A first problem of the first conventional method is in that the data type cannot be correctly verified in a primitive machine instruction set having instructions that allow a plurality of data types to be used. In other words, in the first conventional method, if data type of an instruction in a virtual execution is different at the same point of a program code, a verification error takes place. In addition, even if the first conventional method is applied to an instruction that has a plurality of data types, since the algorithm of the first conventional method does not re-execute an instruction, a varied data type cannot be re-verified.
A second problem of the first conventional method is in that the data type of a local variable cannot be correctly verified. This is because a stack snapshot stored for verifying a program code does not contain the state of a local variable. Thus, for a branch instruction, a local variable area cannot be matched. Even if a local variable contains data that remarkably violates the data type, it cannot be detected in the first conventional method.
On the other hand, a first problem of the second conventional method is in that an execution time may be very long corresponding to a program code. In other words, whenever a data type restriction range is changed for data of each stack, a virtual execution should be repeatedly performed for a stack snapshot. This problem deteriorates the effectiveness of the execution of a program code against a major object of the first conventional method.
A second problem of the second conventional method is in that since type information of unnecessary local variables is continuously stored, the storage capacity of a storing unit is wasted. This is because since a local variable that will be not be used cannot be detected, its information cannot be erased.
Thus, before a program code of a primitive machine instruction set that has instructions allowing a plurality of data types to be used is executed, data type restrictions of the individual instructions of the program code cannot be effectively verified.
An object of the present invention is to solve the above-described problems and to quickly and securely verify a program code of a primitive machine instruction set having instructions that allow a plurality of data types to be used as a data type restriction rage without need to re-execute the program code.
Another object of the present invention is to accurately obtain an effective range of individual data portion so as to effectively use a storing unit.
A first aspect of the present invention is a program verifying system for virtually verifying a program code described as a program instruction set having instructions with data type restrictions so as to determine whether or not the restrictions are correctly satisfied, comprising a data type inferring means for designating a lower limit type permissible as type information for various data types as virtually verified results and un upper limit type corresponding to the use of the data so as to infer the range of the type of each data, a merging means for merging data at a merged point of a plurality of paths due to a branch instruction in the program code and setting a common portion of the data as new data, a forward reflecting means for reflecting the change of the data to the other data that is influenced by the change of the data when the data is changed by the merging means, a forward correlating means for correlating original data and the data changed by the merging means so as to allow the forward reflecting means to select data to be reflected, and a determining means for prohibiting the program code from being really executed when the data type inferring means detects a portion that violates the type restriction in the verified program code.
A second aspect of the present invention is a storage area managing system using a system for virtually executing a program code before really executing the program code, the storage area managing system comprising a virtual executing means for verifying only a data type restriction of the program code before really executing the program code, a data valid range deciding means for deciding the final use position of each data and storing it during the process of the virtual executing means, and a storage area unallocating means for unallocating a storage area for data that exceeds the data valid range corresponding to the data validity range information designated by the data valid range deciding means during the real execution of the program code.
A third aspect of the present invention is an external storage area referencing and managing system for allowing a particular process other than a real execution of a program code to reference data in a system for verifying that the restriction of type information of the program code is not violated so as to omit the type information process in the real execution of the program code, the external storage area reference managing system comprising a virtual executing means for virtually executing the program code from the beginning to the currently executed point corresponding to the currently executed point in the real execution of the program code and corresponding to the data position information to which the particular process references, and a type information restoring means for restoring the data type information to which the virtual executing means references.
A fourth aspect of the present invention is a program verifying method for virtually verifying a program code described as a program instruction set having instructions with data type restrictions so as to determine whether or not the restrictions are correctly satisfied, comprising the steps of (a) designating a lower limit type permissible as type information for various data types as virtually verified results and un upper limit type corresponding to the use of the data so as to infer the range of the type of each data, (b) merging data at a merged point of a plurality of paths due to a branch instruction in the program code and setting a common portion of the data as new data, (c) reflecting the change of the data to the other data that is influenced by the change of the data when the data is changed at step (b), (d) correlating original data and the data changed at step (b) so as to allow data to be reflected to be selected at step (c), and (e) prohibiting the program code from being really executed when a portion that violates the type restriction in the verified program code is detected at step (a).
A fifth aspect of the present invention is a storage area managing method using a system for virtually executing a program code before really executing the program code, the method comprising the steps of (i) verifying only a data type restriction of the program code before really executing the program code, (j) deciding the final use position of each data and storing it at step (i), and (k) unallocating a storage area for data that exceeds the data valid range corresponding to the data validity range information designated at step (j) during the real execution of the program code.
A sixth aspect of the present invention is an external storage area referencing and managing method for allowing a particular process other than a real execution of a program code to reference data in a system for verifying that the restriction of type information of the program code is not violated so as to omit the type information process in the real execution of the program code, the external storage area reference managing method comprising the steps of (l) virtually executing the program code from the beginning to the currently executed point corresponding to the currently executed point in the real execution of the program code and corresponding to the data position information to which the particular process references, and (m) restoring the data type information referenced at step (l).
A seventh aspect of the present invention is a storage medium from which a computer reads a program for virtually verifying a program code described as a program instruction set having instructions with data type restrictions so as to determine whether or not the restrictions are correctly satisfied, the program causing the computer to perform the steps of (a) designating a lower limit type permissible as type information for various data types as virtually verified results and un upper limit type corresponding to the use of the data so as to infer the range of the type of each data, (b) merging data at a merged point of a plurality of paths due to a branch instruction in the program code and setting a common portion of the data as new data, (c) reflecting the change of the data to the other data that is influenced by the change of the data when the data is changed at step (b), (d) correlating original data and the data changed at step (b) so as to allow data to be reflected to be selected at step (c), and (e) prohibiting the program code from being really executed when a portion that violates the type restriction in the verified program code is detected at step (a).
An eighth aspect of the present invention is a storage medium from which a computer reads a program using a system for virtually executing a program code before really executing the program code, the program causing the computer to perform the steps of (i) verifying only a data type restriction of the program code before really executing the program code, (j) deciding the final use position of each data and storing it at step (i), and (k) unallocating a storage area for data that exceeds the data valid range corresponding to the data validity range information designated at step (j) during the real execution of the program code.
A ninth aspect of the present invention is a storage medium from which a computer reads a program for allowing a particular process other than a real execution of a program code to reference data in a system for verifying that the restriction of type information of the program code is not violated so as to omit the type information process in the real execution of the program code, the program causing the computer to perform the steps of (l) virtually executing the program code from the beginning to the currently executed point corresponding to the currently executed point in the real execution of the program code and corresponding to the data position information to which the particular process references, and (m) restoring the data type information referenced at step (l).
These and other objects, features and advantages of the present invention will become more apparent in light of the following detailed description of a best mode embodiment thereof, as illustrated in the accompanying drawings.